i:. |i| = |-i|   

latex

ProofTree

Definitions	P  Q, t  T, i =  j, x:A. B(x), P  Q, P  Q, P & Q, P  Q
Lemmas	absval eq